(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun f () Bool)
(declare-fun g () String)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun aa () Bool)
(assert (not (= "" (str.substr d 0 (str.len e)))))
(assert (= i (= "-" (str.substr d 0 (str.len e)))))
(assert (= (= b f) (= "-" e)))
(assert (= j (= b c)))
(assert (= aa (= "" (str.substr d 0 (str.len e)))))
(assert (= a (= h f)))
(assert b)
(assert (= d (str.++ e g)))
(check-sat)
